package Project;
import java.awt.event.KeyEvent;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.io.PrintWriter;
import java.util.ArrayList;

import ADTs.FileADT;

/**
 * A class to handle saving, loading and various other functionalities 
 * related to save files.
 * 
 * @author	Brian Wetherbee
 * 			Ryan McNamara
 * 			Zeng Yang
 */
public class SaveFile {
	
	private SaveFile(){
		setFileLoaded(false);
		setCurrentFile(null);
	}
	
	/*@
	  @ private invariant fileLoaded == true ==> currentFile != Null;
	  @ private invariant fileLoaded == false ==> currentFile == Null;
	  @*/
	
	//true if a file is Loaded, false otherwise
	private static boolean fileLoaded;
	private static int numberOfFiles = -1;
	
	private static /*@ nullable @*/FileADT currentFile;
	 
	/*@ requires true
	  @ ensures \result > 0
	 @*/
	private static int findNumberOfFiles(){
		int result=-1;
		try {
		    BufferedReader in = new BufferedReader(new FileReader(Constants.SaveFileDir + "info.txt"));
		    String str = in.readLine();
		    result = Integer.parseInt(str);
		    in.close();
		} catch (IOException e) {
		}
		return result;
	}
	
	/*@requires true
	  @ensures findNumberOfFiles() == (\old this).findNumberOfFiles(); 
	 @*/
	private static void increaseNumberOfFiles(){
		try {
			int numFiles = findNumberOfFiles() + 1;
			FileWriter outFile = new FileWriter(Constants.SaveFileDir + "info.txt");
			PrintWriter out = new PrintWriter(outFile);

			out.print(numFiles + "\n");
			
			out.close();
			outFile.close();
			
		} catch (IOException e) {
			e.printStackTrace();
		}
		return;
	}
	
	
	/*@ requires set == true ==> SaveFile.fileLoaded == false;
	  @ requires fileno <= Integer.parseInt((new BufferedReader(new FileReader("info.txt"))).readLine());
	  @ assignable currentFile;
	  @ ensures \result != null;
	  @ ensures set ==> fileLoaded == true;
	  @ ensures !set ==> fileLoaded == false;
	  @ ensures set == false ==> currentFile == \old(currentFile);
	  @ ensures set == true ==> currentFile == \result;
	  @*/
	public static FileADT LoadFile(int fileno,boolean set) {
		
		FileADT loadedFile = null;
		
        try
        {
           FileInputStream fileIn = new FileInputStream(Constants.SaveFileDir + "save"+fileno+".ser");
           ObjectInputStream in = new ObjectInputStream(fileIn);
           loadedFile = (FileADT) in.readObject();
           in.close();
           fileIn.close();
       }catch(IOException i)
       {
           i.printStackTrace();
           return null;
       }catch(ClassNotFoundException c)
       {
           System.out.println("FileADT class not found.");
           c.printStackTrace();
           return null;
       }
       if(set){
    	   fileLoaded = true;
    	   currentFile = loadedFile;
       }
       
       if(set){
    	   saveControlsToConstants();
       }
		
		return loadedFile;
	}
	
	/*@ requires SaveFile.fileLoaded == true;
	  @ ensures SaveFile.fileLoaded == false;
	  @ ensures_redundantly SaveFile.currentFile == null;
	 */
	public static void UnLoadCurrentFile(){
		fileLoaded = false;
		currentFile = null;
		Constants.setDefaultConstrols();
	}
	
	/*@ requires SaveFile.fileLoaded == true;
	  @ requires_redundantly SaveFile.currentFile != null;
	  @ assignable \nothing;
	  @*/
	public static void SaveCurrentFile(){
		try {
			FileOutputStream fileOut = new FileOutputStream(Constants.SaveFileDir + "save" + currentFile.getFileNo()
					+ ".ser");
			ObjectOutputStream out = new ObjectOutputStream(fileOut);
			out.writeObject(SaveFile.currentFile);
			out.close();
			fileOut.close();
		} catch (IOException i) {
			i.printStackTrace();
		}

		return;
	}
	
	
	
	/*@ requires SaveFile.fileLoaded == false;
	  @ ensures \result != null;
	  @ ensures \result == SaveFile.currentFile;
	  */
	public static FileADT CreateNewFile() {
		FileADT newfile = new FileADT();
		try {
			FileOutputStream fileOut = new FileOutputStream(Constants.SaveFileDir + "save" + newfile.getFileNo()
					+ ".ser");
			ObjectOutputStream out = new ObjectOutputStream(fileOut);
			out.writeObject(newfile);
			out.close();
			fileOut.close();
		} catch (IOException i) {
			i.printStackTrace();
		}
		increaseNumberOfFiles();
		
		SaveFile.currentFile = newfile;

		return newfile;
	}
	
	
	/*@requires true
	  @ensures true
	  @*/
	public static void setDefaultConstrols(){
		currentFile.controlUp = java.awt.event.KeyEvent.VK_W;
		currentFile.controlDown = java.awt.event.KeyEvent.VK_S;
		currentFile.controlLeft = java.awt.event.KeyEvent.VK_A;
		currentFile.controlRight = java.awt.event.KeyEvent.VK_D;
		currentFile.controlConfirm = java.awt.event.KeyEvent.VK_ENTER;
		currentFile.controlCancel = java.awt.event.KeyEvent.VK_BACK_SPACE;
		currentFile.controlQuit = java.awt.event.KeyEvent.VK_ESCAPE;
		currentFile.controlUpgrade = java.awt.event.KeyEvent.VK_Q;
		currentFile.controlCustomize = java.awt.event.KeyEvent.VK_E;
		currentFile.controlToggleFullScreen = KeyEvent.VK_F12;
	}

	
	/*@ requires true
	  @ ensures Constants.controlUp == currentFile.controlUp;
	  @ ensures Constants.controlDown == currentFile.controlDown;
	  @ ensures Constants.controlLeft == currentFile.controlLeft;
	  @ ensures Constants.controlRight == currentFile.controlRight;
	  @ ensures Constants.controlConfirm == currentFile.controlConfirm;
	  @ ensures Constants.controlCancel == currentFile.controlCancel;
	  @ ensures Constants.controlQuit == currentFile.controlQuit;
	  @ ensures Constants.controlUpgrade == currentFile.controlUpgrade;
	  @ ensures Constants.controlCustomize == currentFile.controlCustomize;
	  @ ensures Constants.controlToggleFullScreen == currentFile.controlToggleFullScreen;
	  @ ensures SaveFile.SaveCurrentFile();
	  @ assignable Constants.controlUp,
		Constants.controlDown,
		Constants.controlLeft,
		Constants.controlRight,
		Constants.controlConfirm,
		Constants.controlCancel,
		Constants.controlQuit,
		Constants.controlUpgrade,
		Constants.controlCustomize,
		Constants.controlToggleFullScreen;
	 @*/
	public static void saveControlsToConstants() {
		Constants.controlUp = currentFile.controlUp;
		Constants.controlDown = currentFile.controlDown;
		Constants.controlLeft = currentFile.controlLeft;
		Constants.controlRight = currentFile.controlRight;
		Constants.controlConfirm = currentFile.controlConfirm;
		Constants.controlCancel = currentFile.controlCancel;
		Constants.controlQuit = currentFile.controlQuit;
		Constants.controlUpgrade = currentFile.controlUpgrade;
		Constants.controlCustomize = currentFile.controlCustomize;
		Constants.controlToggleFullScreen = currentFile.controlToggleFullScreen;
	}
	
	//*****GETTERS AND SETTERS******

	private static void setCurrentFile(/*@ nullable @*/FileADT currentFile) {
		SaveFile.currentFile = currentFile;
	}

	public static /*@ nullable @*/FileADT getCurrentFile() {
		return currentFile;
	}

	private static void setFileLoaded(boolean fileLoaded) {
		SaveFile.fileLoaded = fileLoaded;
	}

	public static boolean isFileLoaded() {
		return fileLoaded;
	}

	public static void setNumberOfFiles(int numberOfFiles) {
		SaveFile.numberOfFiles = numberOfFiles;
	}

	/*@requires true
	  @ensures \result = this.findNumberOfFiles();
	 */
	public static int getNumberOfFiles() {
		setNumberOfFiles(SaveFile.findNumberOfFiles());
		if (numberOfFiles < 0) {
			System.err.print("info file corruption\n");
		}
		return numberOfFiles;
	}

	
}
